COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%verify[e89,jmc]		The very idea of program verification
C00021 00003	\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
C00022 ENDMK
C⊗;
%verify[e89,jmc]		The very idea of program verification
\input memo.tex[let,jmc]
\title{THE VERY IDEA OF PROGRAM VERIFICATION}

Here are some questions and answers.

	1.  When did program verification start?

Alan Turing and John von Neumann each showed how to prove the
correctness of a small program by a method later introduced in
general form by Floyd in (1967) and called the method of
inductive assertions.  Turing's proof was in 1948 and von
Neumann's was in 19xx.  Neither was published until long after
the author's death.  Yanov in (1958) gave a propositional
calculus theory of program schemas.  It didn't treat any
form of iteration or recursion.
(McCarthy 1961) was the first published paper devoted
to programs involving recursion and therefore requiring
induction for the proof of correctness.

	2. What was (and is) the goal of program verification?

The goal is to eliminate testing the program on cases by
letting the user debug a computer verifiable proof that
the program meets its specifications.  The idea that
correctness proofs were going to be too long and dull to
be verified by hand was present from the beginning.  Of
course, verifying small programs by hand has educational
and research value.

	3. What are program specifications?

There is no single form of specification.  Here are some
that have been studied for programs that don't interact
with the outside world.

	3.1. Consider first programs that begin and (we hope)
end.  We ignore input and output and consider the values of
the variables at the beginning and at the end.  A common
form of specification is to assume a relation among the
values of the variables at the beginning and assert a relation
among their values at the end.  This was studied by Floyd and
later Hoare and was also the content of the two verifications
by Turing and von Neumann.

	3.2. Consider programs that compute functions, e.g.
LISP programs.  A specification may consist of some algebraic
relations among the functions computed by various programs.
This was introduced in (McCarthy 1961) which was superseded
by (McCarthy 1963).  It is the task for which the
Boyer and Moore (196xx ) theorem prover is most suited.

	3.3. One may prove the termination of a procedure, i.e.
that it doesn't get stuck in a loop.  This is done separately
from proving other properties with some techniques and sometimes
it is incorporated in the proofs of input-output relations or
algebraic relations of programs.

	3.4. The correctness of compilers can be proved.
This involves using definitions of the semantics of the
input and output languages and proving a correspondence
between the computations performed by the source and
object programs.  It is non-trivial, because the
object program needn't terminate if the source program
doesn't.

	3.5. The equivalence of programs may be proved.

	Programs that just compute were the first ones
studied.  The idea that a program is a mathematical
object and that its properties follow from its form
was propounded in (McCarthy 1963) and (Hoare 1969)
with such programs in mind.  We'll get to others
later.

	4. What is the relation between programs and
algorithms?

No formal definition of algorithm as distinct from program has
been agreed upon, although it is generally agreed that a program is a
text.  Most specification formalisms don't distinguish the two
and just treat programs.

	5. How sure can you be of the correctness of a verified
program?

	5.1. The machine may fail.  Sometimes they do, but we
would be a lot better off than we are now if usual reason for
failure of programs to meet their specifications were machine
error.

	5.2. The manual may incorrectly describe the machine.
The correspondence between the hardware design and the
machine order code is also subject to verification.

	5.3. The compiler may be incorrect.  If its specifications
have been verified we still have the previous problems concerning
process of compilation.

	5.4. The program that verifies the proofs of the assertions
about the program may be faulty.  This gives rise to the question
of whether there isn't an infinite regress of of verifications of
verifiers.  There are two answers.  First, the verifier is a
single program, and if it is for extensive use, its verification
may warrant extensive human work.  Second, it is worthwhile to
use the verifier to verify proofs of its own specifications.
In principle, this isn't conclusive.  In fact, the bugs in
verifiers aren't likely to take the form that causes it to
be overconfident of its own correctness.

	5.5. The formal specifications may not really describe
what the person who ordered the program wanted.  How likely this
is depends on the task in question and the state of the art
in program writing.  Redundant specifications help here.

	6. What about programs that interact with the real
world?

	In this connection I want to introduce a new idea---that
of {\it illocutionary} and {\it perlocutionary} program specifications,
by analogy with the treatment of {\it speech acts} by philosophers
and linguists, especially J. L. Austin (1955) and John Searle (1969).
The idea of speech acts is that not all sentences are declarative
and characterized by their truth values.  There are commands,
questions, promises, etc.  The utterance of a promise, among
other things, creates an obligation to fulfill it and is
therefore not merely a statement of intention.

	The distinction between {\it illocutionary} and
 {\it perlocutionary} speech acts is exemplified by by
the distinction between commanding someone to do something
and getting him to do it.  The first is characterized by
what is said, and the second is characterized by what effect
saying it actually has.

	The distinction between {\it illocutionary} and {\it
perlocutionary} program specifications will be explained in
connection with a program to perform some of the functions of an
airport control tower in controlling landings.  Suppose the
program can detect the following.

	a. Requests to land.

	b. Whether an airplane has landed and cleared the runway.

	c. Whether an airplane is too close to the
airplane ahead of it.

	d. Whether an instruction has been properly acknowledged.

	Suppose it can perform the following actions.

	a. Tell a pilot he is cleared to land.

	b. Tell a pilot to follow a specific other airplane.

	c. Tell a pilot to slow down his airplane.

	The landing control program will receive requests to land,
will sequence the airplanes and clear an airplane to land after
the previous airplane has landed and cleared the runway.

	The program's illocutionary specifications relate the
programs inputs outputs and its data structures that describe
the situation.  Whether a program meets its illocutionary
specifications is purely a mathematical question 
verifiable from the text of the program and properties of
the programming language.

	The perlocutionary specification is that the airplanes
land safely.  It involves assumptions about the ability of
the program's sensors to correctly detect where the airplanes
are, the success of the communication media, the obedience
of the pilots, the proper functioning of the airplanes and
the absence of airplanes not using the system.

	Is the landing control program meeting its perlocutionary
specifications a mathematical question?  Unless there is a
mathematical theory of the behavior of pilots and airplanes,
the answer is no.  However, within a mathematical theory
of these matters, the answer can be yes.  In so far as
we use theories of the aspects of the world with which
the program interacts, program verification is just another
branch of applied mathematics, subject to the same
philosophical problems---real or fake---as any other
branch of applied mathematics.

	It will often be useful to have both illocutionary
and perlocutionary specifications for the same program and
to relate them.  For example, our theory of the world may
let us prove that if the program meets its illocutionary
specifications, it will also meet its perlocutionary
programs.

	My opinion is that discussion of program specification
that doesn't make some such distinction in the case of programs
that interact with the world is doomed to confusion.

	7. What is the state of the art?

	8. What problems are holding up progress?

It seems to me that there are two main problems.  The first
is that we need better ways of giving the specifications of
programs, especially those that interact with the world.
I hope the idea of distinguishing {\it illocutionary} and
 perlocutionary specifications will help.

The second is that we need better systems for computer assisted,
computer checked proofs.  For some kinds of LISP programs,
computer checkable proofs of correctness are no more difficult
to write than the programs themselves, often easier.  Both
the Boyer-Moore and the EKL provers have demonstrated this.
For other kinds of theorems, both program correctness and
purely mathematical, the proofs are very hard to construct
and differ substantially from the informal arguments given
by mathematicians.  My opinion is that the reason is that
the informal arguments often have a substantial metamathematical
component, i.e. they are really metamathematical proofs that
proofs exist.  There is no insuperable difficulty here, it's
just that we don't know how to formalize metamathematics
well enough.

	9. In view of the fact that program verification isn't
a widely used commercial technique after almost 30 years,
shouldn't you give up?

No.  There are plenty of scientific and engineering problems
that went much longer than that before being solved.
The question is whether scientific and engineering
progress is being made.  My opinion is that reasonable
progress is being made, but to evaluate that claim
one must consult the actual literature.

	10. What is there to read about the present state
of program verification?


	11. What about the DeMillo, Lipton and Perlis flap
and the Fetzer flap?

Neither paper found relevant detailed consideration of the
program verification literature.  Both relied instead on
general philosophical and sociological considerations.
Therefore, they annoyed practitioners.

	My personal opinion is that both papers were vague
in their intermediate statements though clear enough in
their conclusions.  Arguing about them necessarily led
to recriminations about whether someone's position was
misrepresented.

	I don't agree with either paper's conclusions.
First, program verification is a branch of applied
mathematics and not a branch of sociology.
Second, computer checked 
program verification even
in the present state of the art can greatly increase
confidence in the systems in which the programs are
imbedded.
Third, teaching program verification helps computer
scientists and mere programmers understand the
scientific basis of their practice.
Fourth, the day will come when many contracts for programs will
require computer aided formal verification of at least some of
the specifications.

	11. Should the Fetzer article have been published without
requiring the author to refer more directly to the program
verification literature, say to consider at least one current
textbook?

That's a matter of editorial taste.  One way of arousing
interest in aeronautics would have been to publish an
article proving that the Wright brothers' flight at Kitty
Hawk in 1903 was just an expression of the hobby of two
bicycle mechanics and that airplanes were basically toys
because after 30 years, airplanes still couldn't cross
the Atlantic.  It wouldn't have advanced aviation, but
the resulting controversy would have been entertaining.
Maybe there were such articles.
\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
\smallskip\noindent{This draft of VERIFY[E89,JMC]\ TEXed on \jmcdate\ at \theTime}
%File originated on 12-Sep-89
\vfill\eject\end